\begin{tabbing}
pre{-}p(${\it es}$; $i$; ${\it ds}$; $a$; $p$; $P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))\+
\\[0ex]c$\wedge$ \=((alle{-}at(\=${\it es}$;\+\+
\\[0ex]$i$;
\\[0ex]$e$.((es{-}kind(${\it es}$; $e$) = locl($a$) $\in$ Knd)
\\[0ex]$\Rightarrow$ \=(subtype\_rel(es{-}valtype(${\it es}$; $e$); p{-}outcome($p$))\+
\\[0ex]c$\wedge$ \=(($\uparrow$($P$(es{-}state{-}when(${\it es}$; $e$))))\+
\\[0ex]$\wedge$ (\=es{-}val(${\it es}$; $e$)\+
\\[0ex]=
\\[0ex]random\{2:n\}($p$; $i$; $a$)(es{-}kind{-}index(${\it es}$; locl($a$); $e$))
\\[0ex]$\in$ p{-}outcome($p$))))))
\-\-\-\-\\[0ex]$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.existse{-}ge(\=${\it es}$;\+
\\[0ex]$e$;
\\[0ex]${\it e'}$.((es{-}kind(${\it es}$; ${\it e'}$) = locl($a$) $\in$ Knd)
\\[0ex]$\vee$ \=($\neg$($\forall$$t$:rationals. \+
\\[0ex]$\uparrow$($P$(es{-}state{-}after{-}elapsed(${\it es}$; ${\it e'}$; $t$)))))))))
\-\-\-\\[0ex]$\wedge$ \=(($\forall$$t$:rationals. $\uparrow$($P$(es{-}init{-}elapsed(${\it es}$; $i$; $t$))))\+
\\[0ex]$\Rightarrow$ ($\exists$$e$:es{-}E(${\it es}$). (es{-}loc(${\it es}$; $e$) = $i$ $\in$ Id))))
\-\-\-
\end{tabbing}